| Definitions |  x:A. B(x), P   Q, A || B, Prop, t  T, if b t else f fi, 1of(t), p   q, false, Y, p  q, True, Rplus?(x1), P & Q, Rplus-left(x1), Rplus-right(x1), Rnone?(x1), R-loc(R), Rds(R), Rda(R), p = q, R-base-domain(R), R-frame-compat(A;B), R-interface-compat(A;B), i=j, 2of(t), true, Reffect?(x1), Rframe?(x1), Rframe-x(x1), Reffect-x(x1), Reffect-knd(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Rrframe?(x1), Rrframe-x(x1), Reffect-ds(x1), Rrframe-L(x1), Rsends?(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsends-l(x1), Rsframe-tag(x1), Rsends-g(x1), Rsends-knd(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rpre-ds(x1), Rpre-a(x1), Rsends-dt(x1), Reffect-T(x1), Rsends-T(x1),  x. t(x), P  Q, P Q, SQType(T), {T}, A & B, P Q,  T, R-Feasible(R),  A, R-occurs(R;i;z), R-ds(R;i), R-da(R;i), write-restricted(R;i;k), read-restricted(R; i; y), let x = a in b(x), Top, tag(k), rcv(l,tg), x(s), outl(x), Realizer,  b, f(x)?z, x dom(f), Unit, , deq-member(eq;x;L), reduce(f;k;as), False,  , @loc effect knd(v:T) x := f State(ds) v ,  , , left  right, @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc precondition for a(v:T):P State(ds) v, @loc: k writes only members of L, @loc: k sends only on links in L, @loc: only members of L read x, a = b |
| Lemmas | unit wf, IdLnk wf, Knd wf, decl-state wf, decl-type wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, not wf, read-restricted wf, Rnone wf, write-restricted wf, isrcv wf, fpf-cap wf, R-da wf, lsrc wf, lnk wf, Kind-deq wf, fpf-compatible wf, fpf-single wf, R-ds wf, R-occurs wf, R-Feasible wf, eq id wf, bool wf, iff transitivity, eqtt to assert, assert-eq-id, Id sq, eq id self, bnot wf, eqff to assert, assert of bnot, not functionality wrt iff, Rinit wf, Rframe wf, Rsframe wf, band wf, eq knd wf, assert of band, and functionality wrt iff, assert-eq-knd, bor wf, assert of bor, or functionality wrt iff, bnot thru band, Reffect wf, Rpre wf, Rbframe wf, es realizer wf, fpf wf, Id wf, implies functionality wrt iff, subtype rel wf, R-compat wf, R-compat-Rplus2, fpf-join wf, all functionality wrt iff, fpf-compatible-join-iff, R-compat-da, R-compat-ds, subtype rel transitivity, subtype-fpf-cap-void, fpf-sub-join-left, fpf-sub-join-right, eq lnk wf, assert-eq-lnk, Rsends wf, IdLnk sq, bool cases, bool sq, fpf-join-cap, top wf, lnk-decl wf, fpf-cap-single, Knd sq, squash wf, true wf, isrcv-implies, lnk-decl-cap, tagof wf, deq-member wf, l member wf, assert-deq-member |
Type, f:(State(ds)
T)